(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 4))
(let ((e2 3))
(let ((e3 (- v0)))
(let ((e4 (/ e1 e1)))
(let ((e5 (- e4 e4)))
(let ((e6 (- e4)))
(let ((e7 (/ e1 (- e1))))
(let ((e8 (- e4 e3)))
(let ((e9 (- e7)))
(let ((e10 (/ e1 e2)))
(let ((e11 (< e7 e4)))
(let ((e12 (>= e4 e7)))
(let ((e13 (>= e3 v0)))
(let ((e14 (= e5 e5)))
(let ((e15 (< e7 e8)))
(let ((e16 (>= e8 e6)))
(let ((e17 (>= e6 e5)))
(let ((e18 (> e7 e10)))
(let ((e19 (< e8 e4)))
(let ((e20 (<= e10 e9)))
(let ((e21 (ite e14 e9 e5)))
(let ((e22 (ite e15 e21 e3)))
(let ((e23 (ite e19 v0 e6)))
(let ((e24 (ite e18 e7 e4)))
(let ((e25 (ite e11 e10 e22)))
(let ((e26 (ite e16 e8 e25)))
(let ((e27 (ite e13 e3 e6)))
(let ((e28 (ite e20 e5 e5)))
(let ((e29 (ite e17 e28 v0)))
(let ((e30 (ite e17 e6 e21)))
(let ((e31 (ite e12 e24 e24)))
(let ((e32 (> e29 e31)))
(let ((e33 (> e6 e25)))
(let ((e34 (> e4 e3)))
(let ((e35 (<= e21 e8)))
(let ((e36 (< v0 e5)))
(let ((e37 (= e26 e4)))
(let ((e38 (< e8 e9)))
(let ((e39 (= v0 e5)))
(let ((e40 (distinct e5 e10)))
(let ((e41 (<= e23 e8)))
(let ((e42 (> e8 e3)))
(let ((e43 (< e9 e31)))
(let ((e44 (= e7 e5)))
(let ((e45 (<= v0 e24)))
(let ((e46 (>= e8 e8)))
(let ((e47 (= e25 e23)))
(let ((e48 (> v0 e23)))
(let ((e49 (distinct e8 v0)))
(let ((e50 (distinct e26 e31)))
(let ((e51 (> e8 e21)))
(let ((e52 (distinct e25 e25)))
(let ((e53 (= e30 e24)))
(let ((e54 (= e9 e8)))
(let ((e55 (distinct e6 e10)))
(let ((e56 (<= e5 e23)))
(let ((e57 (>= e23 e22)))
(let ((e58 (= e30 e24)))
(let ((e59 (< e24 e23)))
(let ((e60 (< e5 e24)))
(let ((e61 (> e24 e8)))
(let ((e62 (< e5 e10)))
(let ((e63 (<= v0 e10)))
(let ((e64 (distinct e7 e10)))
(let ((e65 (distinct e27 e5)))
(let ((e66 (= v0 e21)))
(let ((e67 (< e4 e21)))
(let ((e68 (> e4 e10)))
(let ((e69 (> e25 e31)))
(let ((e70 (= e27 e9)))
(let ((e71 (= e6 e3)))
(let ((e72 (> e7 e8)))
(let ((e73 (= e6 e10)))
(let ((e74 (= e22 e26)))
(let ((e75 (distinct e31 e24)))
(let ((e76 (>= e25 e24)))
(let ((e77 (= e31 e4)))
(let ((e78 (distinct e9 e5)))
(let ((e79 (>= e22 e21)))
(let ((e80 (> e27 e4)))
(let ((e81 (> e22 e4)))
(let ((e82 (< e7 e23)))
(let ((e83 (< e31 e8)))
(let ((e84 (= e6 e3)))
(let ((e85 (>= e3 e21)))
(let ((e86 (> e30 e8)))
(let ((e87 (> e7 e4)))
(let ((e88 (> e8 e8)))
(let ((e89 (>= v0 e29)))
(let ((e90 (< e26 e3)))
(let ((e91 (> e25 e5)))
(let ((e92 (<= e31 e24)))
(let ((e93 (distinct e28 e27)))
(let ((e94 (xor e71 e87)))
(let ((e95 (ite e38 e39 e70)))
(let ((e96 (not e16)))
(let ((e97 (ite e77 e62 e94)))
(let ((e98 (=> e80 e54)))
(let ((e99 (or e40 e34)))
(let ((e100 (= e56 e49)))
(let ((e101 (= e86 e59)))
(let ((e102 (and e95 e83)))
(let ((e103 (or e66 e90)))
(let ((e104 (=> e48 e64)))
(let ((e105 (=> e45 e99)))
(let ((e106 (xor e65 e103)))
(let ((e107 (or e14 e35)))
(let ((e108 (=> e92 e104)))
(let ((e109 (or e20 e57)))
(let ((e110 (and e17 e43)))
(let ((e111 (xor e101 e33)))
(let ((e112 (xor e82 e18)))
(let ((e113 (xor e81 e68)))
(let ((e114 (ite e36 e76 e91)))
(let ((e115 (or e102 e11)))
(let ((e116 (and e13 e106)))
(let ((e117 (or e96 e51)))
(let ((e118 (or e116 e72)))
(let ((e119 (not e12)))
(let ((e120 (ite e115 e37 e117)))
(let ((e121 (ite e118 e107 e97)))
(let ((e122 (or e53 e60)))
(let ((e123 (= e98 e109)))
(let ((e124 (ite e73 e41 e50)))
(let ((e125 (not e79)))
(let ((e126 (=> e112 e69)))
(let ((e127 (and e58 e100)))
(let ((e128 (not e55)))
(let ((e129 (= e47 e32)))
(let ((e130 (not e44)))
(let ((e131 (ite e110 e125 e46)))
(let ((e132 (or e119 e42)))
(let ((e133 (xor e85 e111)))
(let ((e134 (=> e75 e74)))
(let ((e135 (ite e108 e84 e63)))
(let ((e136 (= e134 e15)))
(let ((e137 (or e130 e131)))
(let ((e138 (=> e132 e61)))
(let ((e139 (=> e129 e19)))
(let ((e140 (or e121 e78)))
(let ((e141 (xor e88 e135)))
(let ((e142 (xor e113 e137)))
(let ((e143 (not e122)))
(let ((e144 (xor e124 e133)))
(let ((e145 (= e143 e136)))
(let ((e146 (or e140 e89)))
(let ((e147 (or e114 e142)))
(let ((e148 (and e120 e138)))
(let ((e149 (xor e52 e105)))
(let ((e150 (xor e146 e145)))
(let ((e151 (=> e147 e93)))
(let ((e152 (not e150)))
(let ((e153 (ite e67 e151 e67)))
(let ((e154 (ite e128 e153 e126)))
(let ((e155 (or e127 e123)))
(let ((e156 (ite e139 e155 e155)))
(let ((e157 (xor e156 e149)))
(let ((e158 (=> e148 e154)))
(let ((e159 (or e152 e152)))
(let ((e160 (not e157)))
(let ((e161 (=> e141 e160)))
(let ((e162 (xor e161 e158)))
(let ((e163 (not e144)))
(let ((e164 (=> e159 e159)))
(let ((e165 (and e162 e163)))
(let ((e166 (or e165 e165)))
(let ((e167 (not e166)))
(let ((e168 (not e167)))
(let ((e169 (xor e164 e164)))
(let ((e170 (xor e168 e169)))
e170
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
